#include<stdio.h>
int main()
{
    printf("%15d\n",0xABCDEF);
    return 0;
}
